P:({k}). (i:. (j:i. P(j))  P(i))  (i:. P(i)) 

latex

Up	int 1, int 1
Definitions	t  T, x(s), P  Q, , , x:A. B(x), False, A, A  B, i  j , P & Q, i  j < k, {i..j}
Lemmas	le wf, int seg wf, nat wf, nat properties, ge wf